Nuprl Lemma : EVal-atom-free_wf
0,22
postcript
pdf
X
:EventsWithValues{i}. EVal-atom-free{i:l}(
X
)
Prop{i'}
latex
Definitions
t
T
,
f
(
a
)
,
Type
,
x
:
A
.
B
(
x
)
,
AtomFree(
T
;
x
)
,
Knd
,
x
:
A
B
(
x
)
,
Prop
,
Id
,
x
:
A
B
(
x
)
,
P
&
Q
,
AtomFreeDecls(
X
)
,
x
:
A
.
B
(
x
)
,
Top
,
EventsWithValues
Lemmas
EVal
wf
,
Id
wf
,
Knd
wf
,
atom-free
wf
origin
X:EventsWithValues{i}. EVal-atom-free{i:l}(X) 
Prop{i'} X:EventsWithValues{i}. EVal-atom-free{i:l}(X) Prop{i'} Tx:A. B(x)
B(x)
B(x)
x:A. B(x)